\begin{tabbing}
trigger1{-}p(${\it es}$;$T$;$A$;$P$;$i$;$k$;$a$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(es{-}vartype(${\it es}$; $i$; $x$) $\subseteq$r $A$)\+
\\[0ex]\& alle{-}at(${\it es}$;$i$;$e$.(es{-}kind(${\it es}$; $e$) = $k$ $\in$ Knd) $\Rightarrow$ (es{-}valtype(${\it es}$; $e$) $\subseteq$r $T$))
\\[0ex]\& \=alle{-}at(${\it es}$;$i$;${\it e'}$.(es{-}kind(${\it es}$; ${\it e'}$) = locl($a$) $\in$ Knd)\+
\\[0ex]$\Rightarrow$ ($\exists$\=$e$:es{-}E(${\it es}$)\+
\\[0ex](es{-}locl(${\it es}$; $e$; ${\it e'}$)
\\[0ex]\& es{-}kind(${\it es}$; $e$) = $k$ $\in$ Knd
\\[0ex]\& ($\uparrow$($P$(es{-}when(${\it es}$; $x$; $e$),es{-}val(${\it es}$; $e$)))))))
\-\-\\[0ex]\& \=alle{-}at(${\it es}$;$i$;$e$.(es{-}kind(${\it es}$; $e$) = $k$ $\in$ Knd)\+
\\[0ex]$\Rightarrow$ ($\uparrow$($P$(es{-}when(${\it es}$; $x$; $e$),es{-}val(${\it es}$; $e$))))
\\[0ex]$\Rightarrow$ existse{-}at(${\it es}$; $i$; ${\it e'}$.(es{-}kind(${\it es}$; ${\it e'}$) = locl($a$) $\in$ Knd)))
\-\-
\end{tabbing}